T:Type, g:Top, L:T List, f:({x:T| (x  L) }(Top+Top)).
concat(map(x.map(y.g(x,y);Case f(x) of inl(m)  [m] ; inr(x)  nil);L))
~
mapfilter(x.g(x,outl(f(x)));x.isl(f(x));L) 

latex

Definitions	t  T, (x  l), Top, x:A. B(x), mapfilter(f;P;L), S  T, S  T, Prop, {T}, P  Q, P  Q, P  Q, P & Q, P  Q, concat(ll), False, A, True, b, b, , isl(x), Unit, x(s)
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, isl wf, bool wf, bnot wf, assert wf, true wf, not wf, false wf, subtype rel function, cons member, l member wf, top wf